COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00004 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.cb ANOTHER APPROACH TO IGNORANCE


	Chris Goad (ig.upd[kno,cg] Sept 1976) has a first order
axiomatization in which it is possible to prove ignorance.
His main example (following my earlier work) is the Wise Man
Problem, and his formalism is the first one in which it is
possible to prove

Let q be a set of propositions and W a proposition.  We have

W specifies Q ≡ (nec(W Implies Q) ∨ nec(W Implies Not Q))

spec(p,W,Q) ≡ k(p,W Implies Q) ∨ k(p,W Implies Not Q)

spec(p,W,Q1) ∧ spec(p,W,Q2) ⊃ spec(p,W,Q1 And Q2) ∧ spec(p,W,Q1 Or Q2)

spec(p,Q,Q) ⊃ spec(p,W,Not Q)

p sees Q ⊃ k(p,Q)

p sees Q1 ∧ ∃W.(nec(W Implies Q1) ∧ nec(W Implies Not Q)) ⊃ ¬k(p,Q)